<html>
    <head>
        <title></title>
        <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
        <link rel="stylesheet" type="text/css" href="../style.css">
    </head>
    <body>
        <div class="text">
        <h2>Propagator</h2>
        Nach dem Start des Propagators wird in dem Ordner, in dem sich die geöffnete Datei
        befindet, automatisch eine Datei "Prop_package_procedure.adb" erstellt. Diese enthält
        die gleiche Ausgabe, die auch im Tab "Propagiert" angezeigt wird. Es muss also gelten:
        <ul>
            <li> zum gesamten Programm gibt es eine Vor- und eine Nachbedingung</li>
            <li> unmittelbar vor jeder while-Schleife steht eine Invariante</li>
            <li> unmittelbar vor jeder if-Anweisung steht ebenfalls eine Zusicherung
        </ul>
        Unter diesen Voraussetzungen lässt sich durch systematisches Propagieren der
        Zusicherungen auf Basis der Regeln des Hoare-Kalküls ein vollständig annotiertes
        Programm erzeugen<br />
        <br />
        Die Ausgabe entspricht in ihrer Syntax Mini-Ada und ist mit logischen Einrückungen 
        versehen. So lässt sich ohne Probleme weiterverarbeiten, also bspw. mit einem
        Ada-Compiler ausführen.
        </div>
    </body>
</html>
